/**CHeaderFile*****************************************************************

  FileName    [ltl2smv.h]

  PackageName [ltl2smv]

  Synopsis    [A function to run ltl2smv routine.]

  Description [Here we perform a convertion from LTL formula to SMV module.
  The invoker provides the LTL fromula in the form of node_ptr expression. 
  The function 'ltl2smv' will convert this formula to a SMV module, which is 
  also node_ptr MODULE.

  This file provides routines for reducing LTL model
  checking to CTL model checking. This work is based on the work
  presented in \[1\]<br>

  <ul><li> O. Grumberg E. Clarke and K. Hamaguchi.  <cite>Another Look
          at LTL Model Checking</cite>. <em>Formal Methods in System
          Design, 10(1):57--71, February 1997.</li>
  </ul>]

  SeeAlso     []

  Author      [Andrei Tchaltsev, Marco Roveri]

  Copyright   [
  This file is part of the ``ltl2smv'' package of NuSMV version 2. 
  Copyright (C) 2005 by ITC-irst. 

  NuSMV version 2 is free software; you can redistribute it and/or 
  modify it under the terms of the GNU Lesser General Public 
  License as published by the Free Software Foundation; either 
  version 2 of the License, or (at your option) any later version.

  NuSMV version 2 is distributed in the hope that it will be useful, 
  but WITHOUT ANY WARRANTY; without even the implied warranty of 
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU 
  Lesser General Public License for more details.

  You should have received a copy of the GNU Lesser General Public 
  License along with this library; if not, write to the Free Software 
  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.

  For more information on NuSMV see <http://nusmv.irst.itc.it>
  or email to <nusmv-users@irst.itc.it>.
  Please report bugs to <nusmv-users@irst.itc.it>.

  To contact the NuSMV development board, email to <nusmv@irst.itc.it>. ]

  Revision    [$Id: ltl2smv.h,v 1.1.4.4 2005/04/20 15:51:30 nusmv Exp $]

******************************************************************************/

#ifndef __LTL_2_SMV_H__
#define __LTL_2_SMV_H__

#include "node/node.h"

/*---------------------------------------------------------------------------*/
/* MACRO declaration                                                         */
/*---------------------------------------------------------------------------*/
/**MAcro********************************************************************

  Synopsis    [This macro is a string represeting the prefix of the name
  of modules generated by ltl2smv procedure]

  Description []

  SeeAlso     [ltl2smv]

******************************************************************************/
#define LTL_MODULE_BASE_NAME "ltl_spec_"

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/
EXTERN node_ptr ltl2smv ARGS((unsigned int uniqueId, node_ptr in_ltl_expr));

#endif /* __LTL_2_SMV_H__ */
